Nuprl Lemma : R-init-rule
0,22
postcript
pdf
i
,
x
:Id,
T
:Type,
v
:
T
. AtomFree(Type;
T
)
@
i
x
initially
v
:
T
||-
es
.@
i
x
initially
v
:
T
latex
Definitions
AtomFree(
T
;
x
)
,
Type
,
Id
,
R
||-
es
.
P
(
es
)
,
P
&
Q
,
x
:
A
B
(
x
)
,
inr(
x
)
,
R-Feasible(
R
)
,
P
Q
,
x
:
A
B
(
x
)
,
@
i
x
initially
v
:
T
,
@
loc
x
initially
v
:
T
,
x
:
A
.
B
(
x
)
,
t
T
,
ES
,
Consistent(
R
;
es
)
,
es
realizer
ind
Rinit
compseq
tag
def
Lemmas
event
system
wf
,
Rinit
wf
,
R-consistent
wf
,
Id
wf
,
atom-free
wf
origin
i, x:Id, T:Type, v:T. AtomFree(Type;T) 
@i x initially v:T ||- es.@i x initially v:T i, x:Id, T:Type, v:T. AtomFree(Type;T) @i x initially v:T ||- es.@i x initially v:T 
B(x)
B(x)
T